COMMENT ⊗   VALID 00008 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.REQUIRE "LSPMAC.PUB[LSP,CLT]" source_file
C00003 00003	.hd206 SPRING 1978
C00006 00004	.if false then begin "hide" 
C00007 00005	.<<hd206 Spring 1978>>
C00010 00006	.bb  Problem 1.
C00017 00007	.bb Problem 2.
C00029 00008	.bb Problem 3.
C00035 ENDMK
C⊗;
.REQUIRE "LSPMAC.PUB[LSP,CLT]" source_file;
.PAGE FRAME 56 HIGH 80 WIDE;
.evenleftborder ← oddleftborder ← 1000;
.area text lines 1 to 56;
.place text;
.
.MACRO  hd206 (TERM) ⊂
.BEGIN    NOFILL  TURNON "←→"
←COMPUTER SCIENCE DEPARTMENT
←STANFORD UNIVERSITY
.SKIP  
CS206  ←COMPUTING WITH SYMBOLIC EXPRESSIONS  →TERM
.TURNOFF
.END ⊃
.
.
.MACRO hw (NUMBER, DUEDATE) ⊂
.   BEGIN TURNON "←"  NOFILL
←PROBLEM SET  NUMBER
←Due  DUEDATE
.   TURNOFF END ⊃
.
.itemmac 1
.
.PORTION MAINPORTION
.
.hd206 SPRING 1978
.skip
.hw 2, |May 16|
.
.bb General comments. 


	This assignment involves proving properties of LISP functions.  
Unless otherwise noted your proofs should be fairly formal.  
The level of detail should be approximately
that of Chapter_III section_7 of the notes.  
For each step of your proof, make sure that 
you list all of the facts (axioms, earlier steps or previously proved properties)
that are necessary to make that step.  
You may use any facts already proved in the notes or in class.

.item←0
.begin   indent 0,6
.bb Assignment.

#. Chapter III.  Exercise 1. ii-v.

#. Chapter III.  Exercise 2. 

#. EXTRA (for practice with extended truth values, not required).
Let ⊗andlist be as defined in Chapter I and assume ⊗p is a suitably well-behaved
predicate.  Prove the following:

	##. ⊗⊗∀u v: [andlis[u*v, p] = andlis[u, p] ∧ andlis[v, p]]⊗

	##. ⊗⊗∀u: [andlis[reverse u, p] = andlis[u, p]]⊗

Hint: define ⊗aandlis, which returns an extended truth value corresponding to
the truth value of ⊗andlis on corresponding arguments.  Show that ⊗andlis
as defined in terms of ⊗aandlis satisfies the desired equivalence.  Then
you may use this result to prove other facts about ⊗andlis.  
The statement that "⊗p is suitably well-behaved" is rather vague.  You will
need to make it more precise in order to make your proof clear.   State this
 in your proof.
.end
.if false then begin "hide" 
.require "lspmac.pub[lsp,clt]" source;
.MACRO  hd206 (TERM) ⊂
.BEGIN    NOFILL  TURNON "←→"
←COMPUTER SCIENCE DEPARTMENT
←STANFORD UNIVERSITY
.SKIP  
CS206  ←COMPUTING WITH SYMBOLIC EXPRESSIONS  →TERM
.TURNOFF
.END ⊃
.
.itemmac 1
.PORTION MAINPORTION
.PAGE ← 1
.end "hide"
.LSPFONT 
.allops
.basicops 
.next page
.<<hd206 Spring 1978>>
.cb Solutions for Problem Set 2.

.bb General comments.

	The following proofs are generally informal and emphasize mainly
the details which are most frequently missed.  In particular,
since the axioms and theorems are stated in terms of sorted variables it 
is important
to understand the implications of this in order not to prove things
which are in fact false.  Thus care has been taken  to point 
out where it is that terms have to
be shown to be of a given sort in order that the axioms, definitions, and
theorems can be applied.  
Problem_3 is worked out in some detail in order to provide an
additional example of the use of representing functions and extended
truthvalues to prove statements
about recursively defined predicates.

	The proofs will be fairly brief in other respects
and in particular the basic LISP axioms will often used without comment.
For example, we will generally use the fact that 
⊗⊗issexp qa u⊗ and ⊗⊗issexp qd u⊗ in the case that ⊗⊗¬qn u⊗ 
without explicit mention.  We will
sometimes justify a step saying "by definition"  which means by using the
functional equation defining the relevant function.  Some simplification 
(of conditional terms etc.) is usually needed to complete the step.

	Most of the proofs are done by list or S-expression induction.  For
example, suppose you wish to prove some property ⊗⊗qP[u]⊗ for all lists ⊗u.  
You first show that qP[qNIL] holds.  Then you assume that ⊗u is not qNIL and
that ⊗⊗qP[qd u]⊗ holds and show that under these assumptions ⊗⊗qP[u]⊗ is
true.  The fact that ⊗⊗qP[u]⊗ holds for all lists ⊗u then follows by list
induction.  The situation for S-expression induction is analogous.
.bb  Problem 1.

	We will use the following facts about the operator < >: 

1.0		⊗⊗∀x: islist <x>⊗   and    ⊗⊗∀x u: <x> * u = x . u⊗

These facts are a simple consequence of the definitions of *, <> and the LISP axioms.  
We will also use the result of Problem 1.i which was proved in class.  

.begin nofill
.bb |Proof of 1.ii         ⊗⊗∀u: islist reverse1 u⊗|

Method:	list induction with   ⊗⊗qP[u] ≡ islist reverse1 u⊗.  

Case ⊗⊗qn u⊗:

    ⊗⊗islist reverse1 u ≡ islist qNIL⊗    ...by definition of ⊗reverse1 
                        ≡ T   ...by the LISP axioms.

Case  ⊗⊗¬qn u⊗ and ⊗⊗islist_reverse1_qd u⊗ 

    ⊗⊗islist reverse1 u ≡ islist [reverse1_qd u_*_<qa u>]⊗   ...by definition  of ⊗reverse1 
                        ≡  T   ...by induction hypothesis, $ISLIST-APPEND and 1.0.

.bb |Proof of 1.iii  ⊗⊗∀u: reverse u = reverse1 u⊗|
	We prove a slightly more general result, namely

1.1		⊗⊗∀u v: reverse1 u * v = rev[u,v]⊗

then taking ⊗v = qNIL the desired result follows by 1.i  and the definition of ⊗reverse.  

Method: list induction with   ⊗⊗qP[u]_≡_∀v:_reverse1_u_*_v_=_rev[u,v]⊗.  

Case  ⊗⊗qn u⊗ 

    ⊗⊗reverse1 qNIL * v = v⊗   ...by definition of ⊗reverse1 and $NIL-APPEND 
                      ⊗⊗= rev[u,v]⊗   ...by definition of ⊗rev .

Case  ⊗⊗¬qn u⊗ and ⊗⊗∀v:_reverse1_qd u_*_v_=_rev[qd u,v]⊗:

    ⊗⊗reverse1 u = reverse1 qd u * <qa u>⊗   ...by definition
		    ⊗⊗= rev[qd u,<qa u>]⊗   ...by induction hypothesis and ⊗⊗islist <qa u>⊗
		    ⊗⊗= rev[u,qNIL]⊗   ...by definition.
.begin fill

	From here on we shall use ⊗reverse and ⊗reverse1 interchangably.  
As 1.iv is more easily proved using 1.v, we will prove 1.v next.
.end
.bb |Proof of 1.v  ⊗⊗∀u v: reverse[u * v] = reverse v * reverse u⊗ |
Method: list induction with ⊗⊗qP[u] ≡ ∀v: reverse[u * v] = reverse v * reverse u⊗. 

Case ⊗⊗qn u⊗:

    ⊗⊗reverse[qNIL * v] = reverse v⊗   ...by $NIL-APPEND  
                   ⊗⊗= reverse v * qNIL⊗   ...by 1.i
                   ⊗⊗= reverse v * reverse qNIL⊗   ...by definition.

Case	⊗⊗¬qn u⊗ and ⊗⊗∀v:_reverse[qd u * v]_=_reverse v * reverse qd u⊗:

    ⊗⊗reverse[u * v] = reverse[qd u * v] * <qa u>⊗   ...by definition, $CAR/CDR-APPEND and ⊗⊗islist u*v⊗
		    ⊗⊗= [reverse v * reverse qd u] * <qa u>⊗   ...by induction hypothesis
		    ⊗⊗= reverse v * [reverse qd u * <qa u>]⊗   ...by $ASSOC-APPEND 
		...here we need ⊗⊗islist reverse v⊗, ⊗⊗islist reverse qd u⊗ and ⊗⊗islist <qa u>⊗
		    ⊗⊗= reverse v * reverse u⊗   ...by definition
 
.bb |Proof of 1.iv   ⊗⊗∀u: reverse reverse u = u⊗ |
Method: list induction with    ⊗⊗qP[u] ≡ reverse reverse u = u⊗.  

Case ⊗⊗qn u⊗:

    ⊗⊗reverse reverse qNIL = reverse qNIL = qNIL⊗   ... by definition

Case    ⊗⊗¬qn u⊗ and ⊗⊗reverse_reverse_qd u_=_qd u⊗:

    ⊗⊗reverse reverse u = reverse[reverse qd u * <qa u>]⊗   ...by definition
		    ⊗⊗= reverse <qa u> * reverse reverse qd u⊗   ... by 1.v
             ...here we need ⊗⊗islist reverse qd u⊗ and ⊗⊗islist <qa u>⊗
		    ⊗⊗= <qa u> * qd u⊗   ...by induction hypothesis and computation  using ⊗⊗islist <qa u>⊗
		    ⊗⊗= u⊗   ...by 1.0 and the LISP axioms

.begin fill
This ends Problem 1 as assigned.  The proof of the equivalence of ⊗flatten and 
⊗fringe as outlined in class is included here for completeness.  
.end
.bb |Proof ⊗⊗∀x u: flat[x,u] = fringe x * u⊗|
Method: S-expression induction with   ⊗⊗qP[x]_≡_∀u:_flat[x,u]_=_fringe_x_*_u⊗.  

Case ⊗⊗qat x⊗:

    ⊗⊗flat[x,u]_=_x_._u⊗    ...by definition
              ⊗⊗= <x> * u⊗   ... by 1.0
              ⊗⊗= fringe x * u⊗  ... by definition

Case   ⊗⊗¬qat x⊗ and ⊗⊗∀u:_flat[qd x,u]_=_fringe_qd x_*_u⊗ :

    ⊗⊗flat[x,u] = flat[qa x,flat[qd x,u]]⊗   ...by definition
		    ⊗⊗= flat[qa x,fringe qd x * u]⊗   ...by induction hypothesis
		    ⊗⊗= fringe qa x * [fringe qd x * u]⊗   ...again by induction hypothesis
                                            ...here we need ⊗⊗islist fringe qd x * u⊗
		    ⊗⊗= fringe x * u⊗   ...by $ISTOT-APPEND and definition of ⊗fringe  
                           ...here we need ⊗⊗islist fringe qd x ⊗ and ⊗⊗islist fringe qa x⊗

.end
.bb Problem 2.

	In proving the desired fact about ⊗subst, ⊗sublis, and @ we will use a new
sort ⊗slist.  The variables ⊗s, ⊗s1, ⊗s2, ⊗s3 range over the domain 
characterized by the predicate ⊗slist.  We axiomatize slists as follows:

2.1 	⊗⊗∀X: [slist X ≡ islist X ∧ [qn X ∨ [¬qat qa X ∧ slist qd X]]]⊗   ...X is a general variable.

Thus ⊗s is either qNIL or a list of nonatomic elements.   We shall also use the
following facts.
.begin nofill

2.2	⊗⊗∀x y: [occur[x,y] ≡ [x=y] ∨ [¬qat y ∧ [occur[x, qa y] ∨ occur[x,qd y]]]]⊗
2.3	⊗⊗∀x s: [qn assoc[x,s] ∨ [issexp assoc[x,s] ∧ ¬qat assoc[x,s]]]⊗
2.4     ⊗⊗∀s1 s2:  slist s1 * s2⊗
2.5	⊗⊗∀z s1 s2: [assoc[z,s1*s2] = qif qn assoc[z,s1] qthen assoc[z,s2] qelse assoc[z,s1]]⊗
2.6	⊗⊗∀x y z: issexp subst[x, y, z]⊗
2.7	⊗⊗∀x,s: issexp sublis[x,s]⊗
2.8	⊗⊗∀s1 s2: slist subsub[s1,s2]⊗
	⊗⊗∀s1 s2:  ¬qn s1 ⊃ ¬qn subsub[s1,s2]⊗
	⊗⊗∀s1 s2:  ¬qn s1 ⊃ qd subsub[s1,s2] = subsub[qd s1,s2]⊗
2.9	⊗⊗∀s1 s2: slist s1@s2⊗
.end
The proof of 2.2 is outlined in the text and 2.3 - 2.9 can be proved by 
straight forward list or S-expression induction using the LISP axioms 
function definitions and 2.1.

.begin nofill
.bb |Proof of 2.i   ⊗⊗∀x y z: subst[x, y, z] = sublis[z, <x,y>]⊗ |

Method: S-expression induction with   ⊗⊗qP[z]_≡_∀x_y:_subst[x,y,z]_=_sublis[z,<x.y>]⊗. 

Case ⊗⊗qat z⊗:

    ⊗⊗subst[x,y,z] = qif y=z qthen x qelse z⊗    ...by definition of ⊗subst 
    ⊗⊗sublis[z,<y.x>] = {assoc[z,<y.x>]}[λz1: qif qn z1 qthen z qelse qd z1]⊗   ... by definition of ⊗sublis 
		    ⊗⊗= qif y≠z qthen z qelse qd y.x⊗    ...by computation since ⊗⊗slist <y.x>⊗.

Case ⊗⊗¬qat z⊗ and ⊗⊗∀x y: [subst[x, y, qa z] = sublis[qa z, <y.x>] ∧ subst[x,y,qd z] = sublis[qd z,<y.x>]]⊗

    ⊗⊗subst[x,y,z] = subst[x,y,qa z] . subst[x,y,qd z]⊗    ...by definition of ⊗subst 
		    ⊗⊗= sublis[qa z, <y.x>] . sublis[qd z,<y.x>]⊗    ...by induction hypothesis
		    ⊗⊗= sublis[z,<y.x>]⊗    ...by definition of ⊗sublis.  


	Before proving (ii) we prove some lemmas.  Namely

2.10	⊗⊗∀z s1 s2: [qn assoc[z, s1] ⊃ assoc[z, s1@s2] = assoc[z,s2]]⊗
2.11	⊗⊗∀z s1 s2:  [¬qn assoc[z,s1] ⊃ ¬qn assoc[z,s1@s2] ∧ qd assoc[z,s1@s2] = sublis[qd assoc[z,s1],s2]⊗
.end

These are fairly simple consequences of the facts mentioned at the beginning of 
this problem and the following statement:
.begin nofill

2.12	⊗⊗∀z s1 s2: [qn assoc[z, s1] ≡ qn assoc[z,subsub[s1,s2]]]⊗
		⊗⊗∧ [¬qn assoc[z,s1] ⊃ qd assoc[z,subsub[s1,s2] = sublis[qd assoc[z,s1],s2]]⊗

.bb |Proof of 2.12.|
Method:  list induction on ⊗s1.  

Case ⊗⊗qn s1⊗:  

    Both sides of the equivalence reduce to ⊗⊗qn qNIL⊗ and the left hand side of ⊃ is F. 


Case ⊗⊗¬qn s1⊗ and ⊗⊗∀z s2: [qn assoc[z, qd s1] ≡ qn assoc[z,subsub[qd s1,s2]]]⊗
                   ⊗⊗∀z s2: [¬qn assoc[z,qd s1] ⊃ qd assoc[z,subsub[qd s1,s2] = sublis[qd assoc[z,qd s1], s2]]⊗

    ⊗⊗assoc[z,subsub[s1,s2]] = qif z=qaa subsub[s1,s2] qthen qa subsub[s1,s2] qelse assoc[z,subsub[qd s1,s2]]⊗ 
           ...by definition of ⊗assoc 
           ...here we need ⊗⊗slist subsub[s1,s2]⊗, ⊗⊗¬qn subsub[s1,s2]⊗ and ⊗⊗qd subsub[s1,s2] = subsub[qd s1,s2]⊗
		⊗⊗= qif z = qaa s1 qthen [qaa s1 . sublis[qda s1,s2]] qelse assoc[z, subsub[qd s1,s2]]⊗
           ...here we need in addition, 2.1, the definition of ⊗subsub and ⊗⊗issexp sublis[qda s1,s2]⊗

Subcase  ⊗⊗z = qaa s1 ⊗:  the result follows from the definitions by computation.

Subcase   ⊗⊗z ≠ qaa s1⊗: the result follows from the induction hypothesis and definition of ⊗assoc.  

.bb |Proof of 2.10|
Assume: ⊗⊗qn assoc[z,s1]⊗ 

    ⊗⊗qn assoc[z, subsub[s1,s2]]⊗    ... by 2.12
    ⊗⊗assoc[z,subsub[s1,s2]*s2]_=_assoc[z,s1@s2]_=_assoc[z,s2]⊗   ...by 2.5 and definition of @. 

.bb |Proof of 2.11|
Assume: ⊗⊗¬qn assoc[z,s1]⊗ 

    ⊗⊗¬qn assoc[z,subsub[s1,s2]]⊗    ...by 2.12
    ⊗⊗assoc[z,s1@s2]_=_assoc[z,subsub[s1,s2]]⊗    ...by 2.5 and definition of @  

The result then follows from the second part of 2.12 and $NOTNIL-APPEND.  

.bb |Proof of 2.ii   ⊗⊗∀z_s1_s2:_sublis[z,s1@s2]_=_sublis[sublis[z,s1],s2]⊗.  |
Method: S-expression induction with ⊗⊗qP[z]_≡_∀s1_s2:_sublis[z,s1@s2]_=_sublis[sublis[z,s1],s2]⊗.

Case ⊗⊗qat z⊗:

    ⊗⊗sublis[z,s1@s2] = {assoc[z,s1@s2]}[λz1: qif qn z1 qthen z qelse qd z1]⊗
    ⊗⊗sublis[z,s1] = {assoc[z,s1]}[λz1: qif qn z1 qthen z qelse qd z1]⊗
.end
If ⊗⊗qn assoc[z,s1]⊗ the result follows from 2.10 and if ⊗⊗¬qn assoc[z,s1]⊗
the result follows from 2.11.
.begin nofill

Case  ⊗⊗¬qat z⊗ and ⊗⊗∀s2: [sublis[qa z, s1@s2] = sublis[sublis[qa z,s1],s2]⊗
		∧ ⊗⊗∀s2: [sublis[qd z, s1@s2] = sublis[sublis[qd z,s1],s2]⊗

    ⊗⊗sublis[z,s1@s2] = sublis[qa z,s1@s2] . sublis[qd z,s1@s2]⊗   ...by definition
		    ⊗⊗= sublis[sublis[qa z,s1],s2] . sublis[sublis[qd z,s1],s2]⊗    ...by induction
		    ⊗⊗= sublis[sublis[z,s1],s2]⊗   ... by definition of ⊗sublis 
           ...here we need ⊗⊗issexp sublis[qa z,s1]⊗ and ⊗⊗issexp sublis[qd z,s1]⊗ 


.bb |Proof of 2.iii ⊗⊗∀z s1 s2 s3: sublis[z, s1@[s2@s3]] = sublis[z, [s1@s2]@s3]]⊗ |
	This is a direct consequence of 2.ii and ⊗⊗slist s1@s2⊗ as follows:

		⊗⊗sublis[z, s1@[s2@s3]] = sublis[sublis[z,s1],s2@s3] ⊗
				⊗⊗= sublis[sublis[sublis[z,s1],s2],s3]⊗
				⊗⊗= sublis[sublis[z,s1@s2],s3]⊗
				⊗⊗= sublis[z, [s1@s2]@s3]⊗

.bb |Proof of 2.iv  ⊗⊗∀x y z: [¬occur[y,z] ⊃ subst[x,y,z] = z]⊗|
Method: S-expression induction with  ⊗⊗qP[z]_≡_∀x_y:_[¬occur[y,z]_⊃_subst[x,y,z]_=_z]⊗.  

Case ⊗⊗qat z⊗:

    ⊗⊗¬occur[y,z]_≡_y≠z⊗ and ⊗⊗subst[x,y,z]_=_qif_y_=_z_qthen_x_qelse_z⊗ so qP holds.  

Case ⊗⊗¬qat z⊗ and ⊗⊗∀x y: [¬occur[y, qa z] ⊃ subst[x,y,qa z] = qa z ∧  [¬occur[y, qd z] ⊃ subst [x,y,qd z]]⊗

    ⊗⊗¬occur[y,z]_≡_y≠z ∧ ¬occur[y,qa z]_∧_¬occur[y,qd z]⊗
    ⊗⊗subst[x,y,z]_=_subst[x,y,qa z]_._subst[x,y,qd z]⊗    ...by definition
                 ⊗⊗= qa z . qd z⊗   ...by induction hypothesis 
                 ⊗⊗= z⊗

%3Proof  of  2.v%1 ⊗⊗∀x  x1  y  y1  z:  [y ≠  y1  ∧  ¬occur[y,  x1]]  ⊃ ⊗
                                    ⊗⊗subst[x1,y1,subst[x,y,z]] = subst[subst[x1,y1,x],y,subst[x1,y1,z]]⊗

Method: S-expression induction on ⊗z.  

Case ⊗⊗qat z⊗:

    ⊗⊗subst[x1,y1,subst[x,y,z]] = qif y=z qthen subst[x1,y1,x] qelse qif y1=z qthen x1 qelse z⊗

    ⊗⊗subst[subst[x1,y1,x],y,subst[x1,y1,z]] ⊗
		⊗⊗= qif y1=z qthen qif y=x1 qthen subst[x1,y1,x] qelse x1⊗
		            ⊗⊗qelse qif y=z qthen subst[x1,y1,x] qelse z⊗
		⊗⊗=qif y1=z qthen x1 qelse qif y=z qthen subst[x1,y1,x] qelse z⊗   ...since  ⊗⊗¬occur[y,x1]⊗

The result now follows by a simple case analysis since ⊗y=z and ⊗y1=z can not both be true.

Case ⊗⊗¬qat z⊗ and ⊗⊗∀x  x1  y  y1:  [y  ≠  y1  ∧  ¬occur[y,  x1]]  ⊃⊗
	⊗⊗subst[x1,y1,subst[x,y,qa z] = subst[subst[x1,y1,x],y,subst[x1,y1,qa z]]⊗
	⊗⊗∧ subst[x1,y1,subst[x,y,qd z] = subst[subst[x1,y1,x],y,subst[x1,y1,qd z]]]⊗ 

    ⊗⊗subst[x1,y1,subst[x,y,z]] = subst[x1,y1,subst[x,y,qa z] . subst[x,y,qd z]]⊗
		⊗⊗= subst[x1,y1,subst[x,y,qa z]] . subst[x1,y1,[subst[x,y,qd z]]⊗
                      ...here we need ⊗⊗issexp subst[x,y,qa z]⊗ and ⊗⊗issexp subst[x,y,qd z]⊗
		⊗⊗= subst[subst[x1,y1,x],y,subst[x1,y1,qa z]] . subst[subst[x1,y1,x],y,subst[x1,y1,qd z]]⊗
		⊗⊗= subst[subst[x1,y1,x],y,subst[x1,y1,z]]⊗

This completes problem 2.
.end

.bb Problem 3.

	We wish to prove the following two statements:

(i)	⊗⊗∀u v: andlis[u*v,phi] ≡ andlis[u,phi] ∧ andlis[v,phi]⊗

(ii)	⊗⊗∀u: andlis[u,phi] ≡ andlis[reverse u,phi]⊗

where ⊗phi is a unary predicate.  (The use of ⊗p in the original porblem statement
was a poor choice as ⊗p is designated in Chapter 3 as a variable of type ⊗istv.)  
Note that even to state this problem requires
an extension to the syntax of our language in order to allow functions that
have functions as arguments.  In the problem ⊗phi is considered as a parameter.
(Quantification over predicates is not allowed.)

	The strategy for doing the proof is as follows.  We define a
representing function ⊗aandlis for ⊗andlis.  To do this we need to know
that ⊗phi has a representing function ⊗pphi.  The statement that ⊗phi is
suitable well behaved becomes then the statement that ⊗pphi maps S-expressions
into the domain $TV and maps general objects into the domain $ETV.  Thus
.nofill

3.1	⊗⊗∀u: [aandlis[u,pphi] = nnull u oor [pphi qa u aand aandlis[qd u,pphi]]⊗
3.2	⊗⊗∀u: isetv aandlis qd u⊗
3.3	⊗⊗∀u: isetv pphi qa u⊗
3.4	⊗⊗∀x: istv pphi x⊗
3.5	⊗⊗∀x: [phi x ≡ pphi x=$$TT$]⊗
3.6	⊗⊗∀u: [andlis[u,phi] ≡ aandlis[u,pphi] = $$TT$]⊗
.fill
Here ⊗nnull is defined similarly to ⊗aatom and we assume the analagous results 
such as $TVNNUL, and $EQNNUL.  
3.2 and 3.3 are needed inorder to be able
to use the definitions of ⊗aand and ⊗oor in the case ⊗⊗qn u⊗. 
Using these axioms we prove

3.7	⊗⊗∀u:_istv_aandlis[u,pphi]⊗ 

from which we get (using $EQAAND $EQOOR etc., and the above axioms)  that

3.8	⊗⊗∀u: [andlis[u,phi] ≡ qn u ∨ [phi qa u ∧ andlis[qd u,phi]]⊗.

This last statement is used together with list induction to prove the desired
results.
.nofill

.bb |Proof of 3.7 |
Method: list induction with ⊗⊗qP[u]_≡_istv_aandlis[u,pphi]⊗.
 
Case ⊗⊗qn u⊗:

    ⊗⊗istv aandlis[u,pphi]_≡_istv $$TT$⊗ ...by  definitions of ⊗nnull, ⊗aand, ⊗oor, 3.1, 3.2 and 3.3 .  

Case ⊗⊗¬qn u⊗  and ⊗⊗istv aandlis[qd u,pphi]⊗:

    ⊗⊗istv aandlis[u,pphi]⊗ follows by definition and $TVOOR from
	⊗⊗[istv nnull u]∧[istv [pphi qa u aand aandlis[qd u,pphi]]⊗
but we have
    ⊗⊗istv [pphi qa u aand aandlis[qd u,pphi]⊗   ...by induction, $TVAND and 3.4 
    ⊗⊗istv [nnull u]⊗   ..by remarks above

.bb |Proof of 3.i.|
Method: list induction with  ⊗⊗qP[u]_≡_∀v:_[andlis[u*v,phi]_≡_andlis[u,phi]_∧_andlis[v,phi]]⊗

Case ⊗⊗qn u⊗:

    ⊗⊗andlis[u*qNIL,phi] ≡ andlis[u,phi]⊗   ...by $NIL-APPEND  
                         ⊗⊗≡ andlis[u,phi] ∧ andlis[qNIL,phi]⊗  ...by 3.8

Case ⊗⊗¬qn u⊗ and ⊗⊗∀v: andlis[qd u*v,phi] ≡ andlis[qd u,phi] ∧ andlis[v,phi]⊗

    ⊗⊗andlis[u*v,phi] ≡ phi qa u ∧ andlis[qd u*v,phi]⊗    ...by $CAR/CDR-APPEND, $ISTOT-APPEND, and 3.8.
                ⊗⊗≡ phi qa u ∧ andlis[qd u,phi] ∧ andlis[v,phi]⊗    ...by the induction hypothesis
		⊗⊗≡ andlis[u,phi] ∧ andlis[v,phi]⊗    ...by 3.8.


.bb |Proof of 3.ii .|
Method: list induction with  ⊗⊗qP[u]_≡_[andlis[u,phi]_≡_andlis[reverse u,phi]]⊗.

Case ⊗⊗qn u⊗:

    ⊗⊗andlis[reverse qNIL,phi] ≡ andlis[qNIL,phi]⊗   ...by definition of ⊗reverse 

Case ⊗⊗¬qn u⊗ and ⊗⊗andlis[reverse qd u,phi] ≡ andlis[qd u,phi]⊗:

    ⊗⊗andlis[reverse u,phi] ≡ andlis[reverse qd u * <qa u>,phi]⊗    ...by definition of ⊗reverse 
		⊗⊗≡ andlis[reverse qd u,phi] ∧ andlis[<qa u>,phi]⊗    ...by (i) 
                        ...here we need ⊗⊗islist reverse qd u⊗ and ⊗⊗islist <qa u>⊗
		⊗⊗≡ andlis[<qa u>,phi] ∧ andlis[qd u,phi]⊗    ...by induction hypothesis
		⊗⊗≡ andlis[u,phi]⊗    ...by  3.8 and properties of <>.
.fill
This completes Problem 3.